$\forall$$T$, $X$:Type, ${\it eq}$:EqDecider($X$), $f$, $g$:$x$:$X$ fp$\rightarrow$ Type, $x$:$X$. $f$ $\subseteq$ $g$ $\Rightarrow$ $f$($x$)?Void $\subseteq\rho$ $g$($x$)?$T$